AWS と定理証明 〜ポリシー言語 Cedar 開発の舞台裏〜
https://fortee.jp/2025fp-matsuri/proposal/8bb407b5-5df3-48bb-a934-0ca6ca628c9a
https://speakerdeck.com/ytaka23/fp-matsuri-2025
組織を横断する 認可 の課題
アプリケーションの各開発チーム
似たような判定を各チームで再発明する
実装は別だが概念として一致させる必要がある
セキュリティ / CCoE チーム
統計的に ガードレール を敷きたい
実装が別なので統一したチェックが困難
上記のような課題を解決するための概念: PDP と PEP
PDP と PEP の両方を併せ持つ一例が Cedar
Cedar の定理証明には LEAN が用いられている
ただし実装自体は Rust
Differential Random Test（DRT）で両者にランダムな同じ値を入力して、結果を比較して Rust - Lean 間の橋渡しをしている
この考え方めちゃくちゃ目から鱗 radish-miyazaki.icon
実装コードと LEAN の橋渡しする際の参考になる
https://gyazo.com/0d764e79b31831cded4bea7f9a54cfa5
Cedar の設計方針
表現力: 典型的なポリシー設計のユースケースをカバー
RBAC: Principle の所属関係に基づく認可
Cedar では Resource もグループ可能
https://gyazo.com/54fbe4ea4a3e381e4868ba07ae8f8e18
in を用いている箇所
ABAC: エンティティ の属性（フィールドに基づく認可）
Cedar ではユーザが自由に設定可能
https://gyazo.com/0a8abe43bb6ca0c938bc0ec9e4af830e
when 内の条件
評価規則の正しさは LEAN で保証されている
安全性: 許可処理の正確性、ポリシー定義のミス防止
記述言語としての汎用性はバグの温床なのでバリデーションチェックは必須
Cedar ではポリシーとは別に提供できる JSON Scheme によるバリデーション
違反したポリシーは登録時にはじかれる
バリデーションは 型チェック で行われている
型システムの正しさは LEAN で保証されている
応答速度: ポリシー数に対してパフォーマンス劣化が起きづらい
Cedar では 以下のような Slice によるパフォーマンス改善
Policy Slice
判定に関わる (Principal, Resource) の組をキーとする辞書データを保持しており、それを基にリクエストに対して無関係なポリシーは除外する
Level-based Entity Slice
ポリシーに無関係なエンティティを除外する
フィールドが辿る必要のある深さをあらかじめ調べる
実際に他の言語（Rego、OpenFAG）と比べるとめちゃくちゃパフォーマンスが高い
特にエンティティ数に対して速度劣化が起きづらい
https://gyazo.com/9efb392f8824011a7dbd7b1e0c155630
最適化の正しさは LEAN を用いて保証されている
解析可能性: 人間だけでなく機械も解析しやすい
Symbolic Compiler（実装中）: https://arxiv.org/pdf/2403.04651
allow / deny とは別にポリシー自体の性質をチェックする
e.g. あるポリシー P1 と別のポリシー P2 は等価か、ポリシー P1 は デッドコード か ...
SMT ソルバ を利用してチェックする ??
ポリシーを SMT ソルバが認識できる形式に変換（エンコーディング）する
e.g. 「2 つのポリシーが異なる結果を返す」ことが SAT（充足可能性）である場合、2 つのポリシーは不等価
SMT ソルバとか SAT について この記事 参考（本発表と同じ方の登壇記事）
エンコードの正しさは LEAN で保証されている
#関数型まつり_2025